Nuprl Lemma : causal-bijection-interleaving
11,40
postcript
pdf
es
:ES,
P
,
Q
:(E
),
f
:({
e
:E|
P
(
e
)}
{
e
:E|
Q
(
e
)} ).
Bij({
e
:E|
P
(
e
)} ;{
e
:E|
Q
(
e
)} ;
f
)
(
e
:{
e
:E|
P
(
e
)} .
e
c
f
(
e
))
e
.
f
(
e
) is c< preserving on
e
.
P
(
e
)
(
e
,
e'
:{
e
:E|
P
(
e
)} . (
(
e'
<
e
))
e
c
e'
)
(
e
,
e'
:{
e
:E|
P
(
e
)} . (
e
<
e'
)
(
a
:{
e
:E|
Q
(
e
)} . ((
e
<
a
) & (
a
<
e'
))))
(
e
:E.
P
(
e
)
(
a
:E.
Q
(
a
)
e
c
a
(
a
<
f
(
e
))
False))
latex
Definitions
P
Q
,
e
c
e'
,
t
...$L
,
False
,
x
.
t
(
x
)
,
t
T
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
x
(
s
)
,
,
x
:
A
.
B
(
x
)
,
A
,
a
.
f
(
a
) is c< preserving on
e
.
P
(
e
)
,
Dec(
P
)
,
Surj(
A
;
B
;
f
)
,
Inj(
A
;
B
;
f
)
,
Bij(
A
;
B
;
f
)
,
{
T
}
,
WellFnd{i}(
A
;
x
,
y
.
R
(
x
;
y
))
Lemmas
es-causl
irreflexivity
,
decidable
es-E-equal
,
es-le
weakening
eq
,
es-causle
weakening
locl
,
es-causl
transitivity2
,
es-causle
weakening
,
decidable
es-causl
,
es-causl-wellfnd
,
false
wf
,
event
system
wf
,
es-E
wf
,
biject
wf
,
causal-order-preserving
wf
,
es-causle
wf
,
not
wf
,
es-causl
wf
origin